$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$), $x$:Atom1.
\\[0ex]($\uparrow$isl(st{-}lookup(${\it tab}$;$x$))) $\Leftarrow\!\Rightarrow$ ($\exists$$n$:\{0..$\parallel$${\it tab}$$\parallel$ $^{-}$\}. (($n$ $\leq$ ptr(${\it tab}$)) \& st{-}atom(${\it tab}$;$n$) = $x$))